\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)), ${\it Config}$:AbsInterface(chain\_config()),\+
\\[0ex]$u$:(\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} $\rightarrow$\{$e$:E$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Config}$))\} ).
\-\\[0ex]update{-}antecedent\{i:l\}(${\it es}$;${\it Cmd}$;${\it Sys}$;${\it Config}$;$u$) $\in$ $\mathbb{P}$
\end{tabbing}